ds:x:Id fp Type, da:k:Knd fp Type, i:Id, es:ES.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1, e2, e:E.
 (loc(e2) = i  loc(e1) = i  e  e2   es-hist{i:l}(es;e1;e)  es-hist{i:l}(es;e1;e2)) 

latex

Definitions

l1  l2, x:A. B(x), t  T, S  T, [e, e'], b, P  Q, False, A, es-info(es;e), event-info(ds;da), es-hist{i:l}(es;e1;e2), x. t(x), a:A fp B(a), Knd, ES, Top, IdDeq, f(x)?z, vartype(i;x), kind(e), KindDeq, valtype(e), Prop, e  e' , loc(e), Id, E, {T}, SQType(T), P  Q, Dec(P), Trans x,y:T. E(x;y), P  Q, P & Q, P  Q, (e <loc e'), strong-subtype(A;B)

Lemmas

iseg-subtype, strong-subtype-set3, strong-subtype-self, nil iseg, decidable es-locl, es-le-not-locl, not wf, es-locl wf, not functionality wrt iff, es-locl-iff, es-interval-nil, iseg wf, es-le-trans, es-interval-iseg, decidable es-le, Id sq, es-le wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, Knd wf, fpf wf, iseg map, event-info wf, es-info wf, es-le-loc, es-loc-pred, es-interval wf, es-interval wf2, es-E wf, Id wf, es-loc wf